# include <stdio.h>
# include <stdlib.h>
# include <math.h>
# include <strings.h>

#include "ptq.h"

/*********************
 STRUCTURES DE DONNEES
      LE MODELE
 *********************/

/* Constantes */
char* tab_cte[100];
/* Predicats a un argument */
char* tab_pred1[300];
/* Predicats a deux arguments */
char* tab_pred2[300];
/* Nombre courant de constantes */
int nb_cte;
/* Nombre courant de predicats unaires */
int nb_pred1;
/* Nombre courant de predicats binaires */
int nb_pred2;
/* Formules atomiques à partir de prédicats unaires */
int pred_unaire[300][100];
/* Formules atomiques à partir de prédicats binaires */
int pred_binaire[300][100][100];

/************************
 	LISTES 
 	  et 
 FONCTIONS SUR LES LISTES
 ************************/

/* Listes d'entiers */
typedef struct{
    int entier;
    struct liste* next;
}liste;

/* Taille d'une liste d'entiers */
int taille(liste* li){
	int n=0;
	while(li){
		n=n+1;
		li=(liste*)li->next;
	}
	return n;
}

/* Ajout d'un entier à une liste d'entiers */
void ajouter_liste(int e, liste** li){
	liste* lii = (liste*)malloc(sizeof(liste));
	lii->entier=e;
	lii->next=*li;
	*li=lii;
}

/* Affichage d'une liste d'entiers */	
void affiche_liste(liste* tmp){
	printf("[");
	//liste* tmp = li;
	while(tmp){
		printf("%i",tmp->entier);
		tmp=(liste*)tmp->next;
		if(tmp)
			printf("-");
		}
	printf("]");
}

/***************
 AJOUT AU MODELE
 ***************/      

/* Ajout d'une constante au modele */
void ajouter_cte(char* s){
    tab_cte[nb_cte]=s;
    tracef(3,"MOD : (%s,%d) ajoute au modele.\n",s,nb_cte);
    nb_cte++;
}

/* Ajout d'un predicat unaire au modele */
void ajouter_pred1(char* s){
    tab_pred1[nb_pred1]=s;
    tracef(3,"MOD : (%s/1,%d) ajoute au modele.\n",s,nb_pred1);
    nb_pred1++;
}

/* Ajout d'un predicat binaire au modele */
void ajouter_pred2(char* s){
    tab_pred2[nb_pred2]=s;
    tracef(3,"MOD : (%s/2,%d) ajoute au modele.\n",s,nb_pred2);
    nb_pred2++;
}

/* Ajout d'un predicat au modele selon son arite*/
void ajouter_pred(char* s, int ar){
	switch(ar){
		case 1:
			ajouter_pred1(s);
			break;
		case 2:
			ajouter_pred2(s);
			break;
		default:
			printf("! Il n'existe pas de predicat d'arite %i !\n",ar);
			break;
	}
}

/*******************
 ELEMENTS et INDICES
 *******************/

/* Indice d'une constante (chaine de caracteres) */
int getID_cte(char* s){
    int i;
    for(i=0;i<nb_cte;i++){
        if(strcmp(s,(char*)tab_cte[i])==0){
            return i;
        }
    }
    return -1;
}

/* Indice d'un predicat unaire (chaine de caracteres) */
int getID_pred1(char* s){
    int i;
    for(i=0;i<nb_pred1;i++){
        if(strcmp(s,(char*)tab_pred1[i])==0){
            return i;
        }
    }
    return -1;
}

/* Indice d'un predicat binaire (chaine de caracteres) */
int getID_pred2(char* s){
    int i;
    for(i=0;i<nb_pred2;i++){
        if(strcmp(s,(char*)tab_pred2[i])==0){
            return i;
        }
    }
    return -1;
}

/**********************
     CORRESPONDANCE
 MODELE / ARBRE LOGIQUE
 **********************/

/* Renvoi du noeud de type PRD dont la valeur est le nom du prédicat en argument. */
noeud* pred2noeud(char* s){
	return cree_n(PRD,(int)s,0,0);
}

/* Renvoi du noeud de type CTE dont la valeur est le nom de la constante en argument. */
noeud* arg2noeud(char* s){
	return cree_n(CTE,(int)s,0,0);
}


/*******************
 AFFICHAGE DU MODELE
 *******************/
 
/* Affichage des formules unaires */
void affiche_pred1(){
    printf("| FORMULES UNAIRES:");
    int i,j;
    char* s;
    char* a1;
    for(i=0;i<nb_pred1;i++){
        //printf("**\n");
        for(j=0;j<nb_cte;j++){
            //printf("***\n");
            //printf("%d - ",i);
            //printf("%d",j);
            int n=pred_unaire[i][j];
            //printf(">%d\n",n);
            if((int)n==1){
                s=tab_pred1[i];
                a1=tab_cte[j];
                //printf(s);
                //printf(a1);
                printf("\n|\t%s(%s).",s,a1);
            }
        }
    }
    printf("\n");
}
 
/* Affichage des formules binaires */
void affiche_pred2(){
    printf("| FORMULES BINAIRES:");
    int i,j,k;
    char* s;
    char* a1;
    char* a2;
    for(i=0;i<nb_pred2;i++){
        for(j=0;j<nb_cte;j++){
            for(k=0;k<nb_cte;k++){
                int n=pred_binaire[i][j][k];
                if((int)n==1){
                    s=tab_pred2[i];
                    a1=tab_cte[j];
                    a2=tab_cte[k];
                    printf("\n|\t%s(%s,%s).",s,a1,a2);
                }
            }
        }
    }
    printf("\n");
}

/* Affichage des constantes */
void affiche_list_cte(){
    int i,j,k;
    printf("| CONSTANTES:\n");
    for(i=0;i<nb_cte;i++){
        printf("|\t%i: %s\n",i,(char*)tab_cte[i]);
    }
}

/* Affichages des prédicats unaires */
void affiche_list_pred1(){
    int i,j,k;
    printf("| PREDICATS UNAIRES:\n");
    for(i=0;i<nb_pred1;i++){
        printf("|\t%i: %s\n",i,(char*)tab_pred1[i]);
    }
}

/* Affichage des prédicats binaires */
void affiche_list_pred2(){
    int i,j,k;
    printf("| PREDICATS BINAIRES:\n");
    for(i=0;i<nb_pred2;i++){
        printf("|\t%i: %s\n",i,(char*)tab_pred2[i]);
    }
}

/* Affichage du modele */
void affiche_modele(){
	printf("MODELE :\n");
    affiche_list_cte();
    affiche_list_pred1();
    affiche_pred1();
    affiche_list_pred2();
    affiche_pred2();
}
  
/* Affichage des proprietes d'une constante donnee */
void affiche_prop_cte(char* s){
    int i,j,k;
    char* p;
    int n = getID_cte(s);
    char* a1;
    char* a2;
    printf("| LES PROPRIETES DE \'%s\':\n",s);
    for(i=0;i<nb_pred1;i++){
	if(pred_unaire[i][n]==1){
		p=tab_pred1[i];
		printf("|\t%s(%s).\n",p,s);
		}
	}
    for(i=0;i<nb_pred2;i++){
        for(j=0;j<nb_cte;j++){
            for(k=0;k<nb_cte;k++){
            	if(n==j){
            		if(pred_binaire[i][n][k]==1){
 				p=tab_pred2[i];
 				a2=tab_cte[k];
				printf("|\t%s(%s,%s).\n",p,s,a2);
				}
			}
		}
	    }
        for(j=0;j<nb_cte;j++){
            for(k=0;k<nb_cte;k++){
            	if(n==k){
            		if(pred_binaire[i][j][k]==1){
 				p=tab_pred2[i];
 				a1=tab_cte[j];
				printf("|\t%s(%s,%s).\n",p,a1,s);
				}
			}
		}
	    }
	}	               			
}

/***************************
 AJOUT, RETRAIT et RECHERCHE
    de formules au modele
 ***************************/
 
/* Seules les formules "positives" sont enregistrees dans le modele.
 * L'absence d'une formule dans le modele correspond a la negation de cette formule.
 */

/* Ajout et Retrait d'une formule au modele
 * Arguments: 	
 *	- pred: predicat de la formule.
 *	- args: liste d'entiers correspondants aux indices des constant.
 * 	- verite: 1=ajout 0=retrait.
 */ 
void ajouter_terme(int pred,liste* args, int verite){
    int n=taille(args);
    int a1,a2,a3;
    liste* li;
    int ancienne_verite;
    	switch(n){
        	case 1:
            		a1=args->entier;
            		ancienne_verite=pred_unaire[pred][a1];
            		//printf("verite > %i | ancienne > %i\n",verite,ancienne_verite);
            		if(verite+ancienne_verite==1){
           			pred_unaire[pred][a1]=verite;
	    			if(verite==1)
					tracef(3,"MOD : %s(%s) ajoute au modele.\n",tab_pred1[pred],tab_cte[a1]);
				else
					tracef(3,"MOD : %s(%s) retire du modele.\n",tab_pred1[pred],tab_cte[a1]);
				}
			else
				tracef(3, "MOD : modele inchange\n");
           		break;
           			
        	case 2:
          	  	a1=args->entier;
         	   	li=(liste*)args->next;
        	    	a2=li->entier;
        	    	ancienne_verite=pred_binaire[pred][a1][a2];
        	    	//printf("verite > %i | ancienne > %i\n",verite,ancienne_verite);
        	    	if(verite+ancienne_verite==1){
        	    		pred_binaire[pred][a1][a2]=verite;
		    		if(verite==1)
					tracef(3,"MOD : %s(%s,%s) ajoute au modele.\n",tab_pred2[pred],tab_cte[a1],tab_cte[a2]);
				else
					tracef(3,"MOD : %s(%s,%s) retire du modele.\n",tab_pred2[pred],tab_cte[a1],tab_cte[a2]);
            			
            		}
            		else
            			tracef(3,"MOD :modele inchange.\n");
            		break;
    		}
}

/* Recherche d'une formule:
 * Arguments:
 * 	- pred: predicat de la formule.
 	- args: liste d'entiers correspondants aux indices des constantes.
 */
int rechercher_terme(int pred,liste* args){
    int n=taille(args);
    int a1,a2,a3;
    liste* li;
    switch(n){
        case 1:
            a1=args->entier;
            return pred_unaire[pred][a1];
            break;
        case 2:
            a1=args->entier;
            li=(liste*)args->next;
            a2=li->entier;
            return pred_binaire[pred][a1][a2];
            break;
    }
}

/***********************
 FONCTIONS D'EVALUATION
 ***********************/

int max(int n, int p){
    if (n>p) return n;
    else return p;}

int abs(int n){
    if (n>0) return n;
    else return (-1)*n;}

int valuation (char p){
    if (p%2==0) return 1;
    else return 0;}

int val_and(int n, int p){
    return n * p;}

int val_or(int n, int p){
    return max(n, p);}

int val_not(int n){
    return (1-n);}

int val_imp(int n, int p){
    if (n==0) return 1;
    else return (p==1);}


/**********
 QUESTIONS
 **********/
 
/* Questionnement du modele sur la veracite d'une formule.
 * Une formule est representee par un arbre logique.
 */
int question(noeud* racine);

 
/* Renvoi de la valeur de verite d'une application fonctionnelle (AF).
 * Arguments:
 * 	- racine: noeud AF.
 * 	- liste d'entiers: listes des indices de constantes sous ce noeud AF.
 * Algorithme:
 * 	- si le type du fils droit de racine est VAR,
 *		prendre la valeur de son fils gauche (qui est de type CTE grace à remplacer_var_question()).
 * 	- SWITCH du type du fils gauche de racine:
 *		PRD: retourner la valeur de verite de la formule composee de ce predicat et de la liste des constantes rencontrees.
 *		AF: appliquer question_af() sur ce noeud et la liste de constantes amelioree par la constante du fils droit de racine.  
 */
int question_af(noeud* racine, liste* li){
	//printf("question_a\n");
	//getchar();
	if (racine == NULL){
       		printf("racine == NULL");
        	return ;}
	noeud* fd0 = racine->fd;
	//getchar();
	if(fd0->type==VAR)
		fd0=fd0->fg;
	//getchar();
	//affiche_formule(racine);
	//getchar();
	noeud* fg0 = racine->fg;
	//getchar();
	if(fd0->type==VAR){
		//affiche_formule(fd0);
		//getchar();
		fd0=fd0->fg;}
	//getchar();
	char* arg = (char*)string_tds(CTE,fd0->val);//tds
	//getchar();
	//printf(">%s",arg);getchar();
	int IDarg = getID_cte(arg);
	//getchar();
	//printf(">%i",IDarg);
	//getchar();
	ajouter_liste(IDarg,&li);
	//getchar();
	char* prd;
	int IDprd;
	int size;
	
	//printf("%i",fg0->type);
	//getchar();
    	switch (fg0->type) {
    		case PRD:
    			prd =(char*)string_tds(PRD,fg0->val);//tds
    			size=taille(li);
    			if(size==1){
    				IDprd=getID_pred1(prd);
    			}
    			else if(size==2){
    				IDprd=getID_pred2(prd);
    				}
    			else{}
                	int n =rechercher_terme(IDprd,li);
    			return n;
    			break;
    		case AF:
    			question_af(fg0,li);
    			break;
	}
}


/* Renvoi de la valeur de verite d'une formule quantifiee par remplacement recursif des variables.
 * Arguments:
 * 	- racine: fils droit d'un noeud QUANT.
 * 	- var: valeur de la variable.
 * 	- s: constante "remplacant" la variable mentionnee.
 * Algorithme:
 * 	- SWITCH du type de la racine:
 *		VAR: ajouter un noeud gauche a racine de type CTE.
 *		PRD,CTE: ne rien faire.
 *		LAMBDA,AF,OP2,OP1: appliquer remplacer_var_question() sur chacun de leur fils.
 *		QUANT: appliquer remplacer_var_question() sur son fils droit,
 *			puis appliquer la fonction de questionnement correspondant au type de QUANT.
 */
int remplacer_var_question(noeud* racine, int var, char* s){
	//printf(">>>%i",racine->type);
	switch(racine->type){
		case VAR:
			//printf("+++");
			//printf("#>%i",racine->val);
			//printf("#<%i",var);
			if((int)string_tds(VAR,racine->val)==var){
				racine->fg=cree_n(CTE,val_tds(s),0,0);
				//affiche_formule(racine);
			}
			break;
		case PRD:
		case CTE:
			break;
		case LAMBDA:
		case AF:
		case EQ:
		case OP2:
			remplacer_var_question(racine->fd,var,s);
		case OP1:
			remplacer_var_question(racine->fg,var,s);
			break;
		case QUANT:
			remplacer_var_question(racine->fd,var,s);
			switch(racine->val){
				case 1: //some
					return question_existe(racine);
					break;
				case 2: //all
					return question_univers(racine);
					break;
				}
			break;
	}
}

/* Renvoi de la valeur de verite d'une formule existentielle.
 * Argument:
 * 	- racine: noeud QUANT de valeur 0 (existentiel).
 * Algorithme:
 * 	- Pour chaque constante du modele:
 		application de remplacer_var_question() sur tous les fils du fils droit de racine,
 		(ajout d'un noeud CTE correspondant à la constante courante, sous chaque variable de meme valeur que la variable du fils gauche de racine).
 * 	- si l'une des formules (ou normalement toutes les variables ont ete constantifiees) est vraie,
 *		renvoyer vrai.
 * 	- sinon, renvoyer faux.
 */			
int question_existe(noeud* racine){
	//printf("***quest_existe***\n");
	noeud* fg0 = racine->fg;
	noeud* fd0 = racine->fd;
	int IDvar=(int)string_tds(VAR,fg0->val);
	//printf("IDvar:%i-",IDvar);
	int i;
	char* arg;
	for(i=0;i<nb_cte;i++){
		arg=tab_cte[i];
		int n=remplacer_var_question(fd0,IDvar,arg);
		//affiche_formule(fd0);
		//printf("\n");
		int qsv = question_sans_var(fd0);
		//printf("\t> %i\n",qsv);
		if(qsv==1)
		//if(n==1) inutile
			return 1;
	}
	return 0;
}

/* Renvoi de la valeur de verite d'une formule universelle.
 * Argument:
 * 	- racine: noeud QUANT de valeur 1 (universel).
 * Algorithme:
 * 	- Pour chaque constante du modele:
 		application de remplacer_var_question() sur tous les fils du fils droit de "racine",
 		(ajout d'un noeud CTE correspondant à la constante courante, sous chaque variable de meme valeur que la variable du fils gauche de racine).
 * 	- si l'une des formules (ou normalement toutes les variables ont ete constantifiees) est fausse,
 *		renvoyer faux.
 * 	- sinon, renvoyer vrai.
 */
int question_univers(noeud* racine){
	//printf("***quest_univ***\n");
	noeud* fg0 = racine->fg;
	noeud* fd0 = racine->fd;
	int IDvar=(int)string_tds(VAR,fg0->val);//tds
	int i;
	char* arg;
	for(i=0;i<nb_cte;i++){
		arg=tab_cte[i];
		int n=remplacer_var_question(fd0,IDvar,arg);
		//affiche_formule(fd0);
		//printf("\n");
		int qsv = question_sans_var(fd0);
		//printf("\t> %i\n",qsv);
		if(qsv==0)
		//if(n==0) inutile
			return 0;
	}
	return 1;
}

/* Renvoi de la valeur de verite d'une formule.
 * Argument:
 * 	- racine: formule traitee.
 * Algorithme:
 * 	- SWITCH du type de racine:
 *		AF: renvoyer la valeur de question_af() avec comme argument "racine" et une "liste vide d'entiers".
 *		LAMBDA: non traite, car on suppose que la beta-reduction nous a debarasse des noeuds de type LAMBDA.
 *		QUANT: appliquer la fonction correspondant à la valeur 0 ou 1 (resp. existentiel ou universel) sur "racine".
 *		OP1: renvoyer la valeur inverse de celle renvoyee par question() appliqué sur le fils gauche de "racine".
 *		OP2: renvoyer la valeur correspondant au calcul de la conjonction/disjonction/implication du fils gauche de "racine" et du fils droit de "racine".
 */
int question(noeud * racine){
	//printf("***QUESTION***\n");
    if (racine == NULL){
        printf("racine == NULL");
        return ;}
    switch (racine->type) {
        case AF:
	       return question_af(racine,NULL);
            break ;
        case LAMBDA:
            printf("MOD : case LAMBDA non traite -> Beta reduction.\n");
            return -1;
            break ;
        case QUANT :
		//printf("QUANT");
            switch(racine->val){
                case 1: //some
                    return question_existe(racine);
      		    break;
                case 2: //all
                    return question_univers(racine);
                    break;
                }
            break ;
        case OP1 : 
		//printf("not ") ;
        	return val_not(question(racine->fg));
	        break ;
        case OP2 :
        	switch(racine->val){
                case 1: // et
        			return val_and(question(racine->fg),question(racine->fd));
        			break;
        	case 2: // ou
        		    	return val_or(question(racine->fg),question(racine->fd));
         			break;
		case 3: // implies
        			return val_imp(question(racine->fg),question(racine->fd));
        			break;
        	}
            break ;
    }
}

/* Renvoi la valeur de verite d'une formule ne contenant que des variables "constantifiees".
 * Argument:
 * 	- racine: fils droit d'un noeud QUANT.
 * Algorithme:
 * 	- SWITCH du type de "racine":
 *		AF: appliquer question_af() sur "racine".
 *		LAMBDA: non traite.
 *		QUANT: appliquer question_sans_var() sur le fils droit de "racine".
 *		OP1: renvoyer la valeur inverse de celle renvoyee par question_sans_var() appliqué sur le fils gauche de "racine".
 *		OP2: renvoyer la valeur correspondant au calcul de la conjonction/disjonction/implication du fils gauche de "racine" et du fils droit de "racine".
 */
int question_sans_var(noeud * racine){
	//printf("***QUESTION SS VAR***\n");
    if (racine == NULL){
        printf("racine == NULL");
        return ;}
        //printf("TYPE: %i\n",racine->type);
        //getchar();
    switch (racine->type) {
        case AF:
	       return question_af(racine,NULL);
            break ;
        case LAMBDA:
            printf("MOD : case LAMBDA non traite -> Beta reduction.\n");
            return -1;
            break ;
        case QUANT :
            return question_sans_var(racine->fd);
            break ;
        case EQ:
        	//printf("*****************************\n");
        	//affiche_formule(racine);
        	//getchar();
        	return (racine->fg->fg->val == racine->fd->fg->val);
        	break;
        case OP1 : 
               	return val_not(question_sans_var(racine->fg));
	        break ;
        case OP2 :
        	switch(racine->val){
                case 1: // et
        			return val_and(question_sans_var(racine->fg),question_sans_var(racine->fd));
        			break;
        	case 2: // ou
        		    	return val_or(question_sans_var(racine->fg),question_sans_var(racine->fd));
         			break;
		case 3: // implies
        			return val_imp(question_sans_var(racine->fg),question_sans_var(racine->fd));
        			break;
        	}
            break ;
    }
}

/* Affichage de la réponse correspondante au questionnement du modele sur une formule.
 * Argument:
 * - racine: formule dont on teste l'existence dans le modele.
 */
void poser_question(noeud* racine){
	int n = question(racine);
	switch(n){
		case 1:
			printf("vrai.\n");
			break;
		case 0:
			printf("faux.\n");
			break;
		case -1:
			printf("pas de reponse.\n");
			break;
		}
}

/***********
 ASSERTIONS
 ***********/
 
/* Assertion d'une formule dans le modele.
 * Une formule est representee par un arbre logique.
 */
void assertion(noeud * racine, int verite);

/* Assertion (dans le modele) d'une formule quantifiee par remplacement recursif des variables.
 * Arguments:
 * 	- racine: fils droit d'un noeud QUANT.
 * 	- var: valeur de la variable.
 * 	- s: constante "remplacant" la variable mentionnee.
 *	- verite: 0 ou 1 (resp. negation ou affirmation).
 * Algorithme:
 * 	- SWITCH du type de "racine":
 *		VAR: ajouter un noeud gauche a "racine" de type CTE.
 *		PRD,CTE: ne rien faire.
 *		LAMBDA,AF,OP2,OP1: appliquer remplacer_var_assertion() sur chacun de leur fils.
 *		QUANT: appliquer remplacer_var_assertion() sur son fils droit,
 *			puis appliquer la fonction d'assertion correspondant au type de QUANT.
 */
void remplacer_var_assertion(noeud* racine, int var, char* s, int verite){
	//printf(">>>%i",racine->type);
	switch(racine->type){
		case VAR:
			//printf("+++");
			//printf("#>%i",racine->val);
			//printf("#<%i",var);
			if((int)string_tds(VAR,racine->val)==var){
				racine->fg=cree_n(CTE,val_tds(s),0,0);
				//affiche_formule(racine);
			}
			break;
		case PRD:
		case CTE:
			break;
		case LAMBDA:
		case AF:
		case OP2:
			remplacer_var_assertion(racine->fd,var,s,verite);
		case OP1:
			remplacer_var_assertion(racine->fg,var,s,verite);
			
			break;
		case QUANT:
			remplacer_var_assertion(racine->fd,var,s,verite);
			switch(racine->val){
				case 1: //some
      		        		printf("MOD : case IL_EXISTE non traite -> Combinatoire des mondes possibles.\n");
      		        		break;
				case 2: //all
					assertion_univers(racine,verite);
					break;
				}
			break;
	}
}

void remplacer_var(noeud* racine, int var, char* s){
	//printf("remplacer_var  %i\n",var);
	//getchar();
	//affiche_formule(racine);
	switch(racine->type){
		case VAR:
			//printf("+++");
			//printf("# a remplacer: %i\n",racine->val);
			//printf("#remplace par: %i\n",var);
			if(racine->val==var){
				racine->fg=cree_n(CTE,val_tds(s),0,0);
				//affiche_formule(racine);
			}
			break;
		case PRD:
		case CTE:
			break;
		case AF: 
			remplacer_var(racine->fd,var,s);
			remplacer_var(racine->fg,var,s);
			break;
		default:
			printf("MOD : -erreur(remplacer_var)-\n");
			break;			
	}
	//printf("remplacer_var ok\n");
}

/* Assertion (dans le modele) d'une formule universelle.
 * Argument:
 * 	- racine: noeud QUANT de valeur 1 (universel).
 *	- verite: 0 ou 1 (resp. negation ou affirmation).
 * Algorithme:
 * 	- Pour chaque constante du modele:
 		- application de remplacer_var_assertion() sur tous les fils du fils droit de "racine",
 		(ajout d'un noeud CTE correspondant à la constante courante, sous chaque variable de meme valeur que la variable du fils gauche de "racine").
 * 		- application de asserion_sans_var() sur le fils droit de "racine" avec "verite".
 */
int assertion_univers(noeud* racine, int verite){
	//printf("\n***ass_univ***\n");
	//affiche_formule(racine);
	noeud* fg0 = racine->fg;
	noeud* fd0 = racine->fd;
	int IDvar=(int)string_tds(VAR,fg0->val);//tds
	int i;
	char* arg;
	for(i=0;i<nb_cte;i++){
		arg=tab_cte[i];
		//printf("CTE >>> %s\n",arg);
		remplacer_var_assertion(fd0,IDvar,arg,verite);
		//affiche_formule(fd0);
		//printf("\n");
		assertion_sans_var(fd0,verite);
	}
}

/* Assertion (dans le modele) d'une application fonctionnelle (AF).
 * Arguments:
 * 	- racine: noeud AF.
 * 	- liste d'entiers: listes des indices de constantes sous ce noeud AF.
 *	- verite: 0 ou 1 (resp. negation ou affirmation).
 * Algorithme:
 * 	- si le type du fils droit de "racine" est VAR,
 *		prendre la valeur de son fils gauche (qui est de type CTE grace à remplacer_var_assertion()).
 * 	- SWITCH du type du fils gauche de racine:
 *		PRD: ajouter au modele la formule composee de ce predicat et de la liste des constantes rencontrees.
 *		AF: appliquer assertion_af() sur ce noeud et la liste de constantes amelioree par la constante du fils droit de racine.  
 */
void assertion_af(noeud* racine,liste* li, int verite){
	//printf("\n*ass_af*\n");
	//affiche_formule(racine);
	if (racine == NULL){
       		printf(" racine == NULL");
        	return ;}
	noeud* fd0 = racine->fd;
	if(fd0->type==VAR)
		fd0=fd0->fg;
	noeud* fg0 = racine->fg;
	char* arg = (char*)string_tds(CTE,fd0->val);//tds
	//printf("\n\tcte: %s\n",arg);
	//affiche_formule(fd0);
	int IDarg = getID_cte(arg);
	ajouter_liste(IDarg,&li);
	char* prd;
	int IDprd;
	int size;
	//printf(">%i\n",fg0->type);
    	switch (fg0->type) {
    		case PRD:
    			prd =(char*)string_tds(PRD,fg0->val);//tds
    			size=taille(li);
    			if(size==1){
    				IDprd=getID_pred1(prd);
    			}
    			else if(size==2){
    				IDprd=getID_pred2(prd);
    				}
    			else{}
    			//ajouter_liste(IDprd,&li);
    			//return li;
			ajouter_terme(IDprd,li,verite);
			
    			break;
    		case AF:
    			assertion_af(fg0,li,verite);
    			break;
	}
}

/* Assertion d'une formule implicative.
 * Arguments:
 *	- racine: noeud dont le type est OP2 de valeur "implies".
 *	- verite: 0 ou 1 (resp. negation ou affirmation).
 */
void assertion_imp(noeud* racine,int verite){
	if(question(racine->fg)){
		assertion(racine->fd,verite);	
	}
}

/* Assertion d'une formule implicative (ou toutes les variables sont constantifiées").
 * Arguments:
 *	- racine: noeud dont le type est OP2 de valeur "implies".
 *	- verite: 0 ou 1 (resp. negation ou affirmation).
 */
void assertion_imp_sans_var(noeud* racine,int verite){
	if(question_sans_var(racine->fg)){
		assertion_sans_var(racine->fd,verite);	
	}
}



/*
 * -1 nest pas de la forme /EQ/	
 * 0 non-unicité => presupposition fausse.
 * 1 unicité => présupposition ok.
 */
int presupposition(noeud* racine,int verite){
	noeud* prems = racine;
	//printf("\n");
	if(racine->fd){
	//printf("\tok\n");
	if(racine->fd->type==OP2){
	//printf("type: %i\n",racine->fd->type);
	//printf("OP2\n");
	if(racine->fd->val==1){
			if(racine->fd->fg){
			//printf("\tok\n");
			if(racine->fd->fg->type==QUANT){
			//printf("type: %i\n",racine->fd->fg->type);
			//printf("QUANT\n");
			//affiche_formule(racine->fd->fg);
			if(racine->fd->fg->val==2){
					if(racine->fd->fg->fd){
					//printf("\tok\n");
					if(racine->fd->fg->fd->type==OP2){
					//printf("type: %i\n",racine->fd->fg->fd->type);
					//printf("OP2\n");
					//affiche_formule(racine->fd->fg->fd);
					if(racine->fd->fg->fd->val==3){
							if(racine->fd->fg->fd->fd){
							//printf("\tok\n");
							if(racine->fd->fg->fd->fd->type==EQ){
							//printf("type: %i\n",racine->fd->fg->fd->fd->type);
							//printf("EQ\n");
							affiche_formule(racine->fd->fg->fd->fg);
							//getchar();
							int compteur=0;
							int i;
							int indice_mem;
							for(i=0;i<nb_cte;i++){
								noeud* tmp = racine->fd->fg->fd->fg;
								remplacer_var(tmp,(int)racine->fd->fg->fg->val,tab_cte[i]);
								//affiche_formule(prems);
								//printf("***********\n");
								//getchar();
								if(question_af(racine->fd->fg->fd->fg,NULL)==1){
									compteur++;
									indice_mem=i;
									}
								}
							//printf(">>> compteur %i\n",compteur);
							if(compteur==1){
								//printf(">>> indice_mem %i - %s\n",indice_mem,tab_cte[indice_mem]);								
								remplacer_var(racine->fd->fg->fd->fg,(int)racine->fd->fg->fg->val,tab_cte[indice_mem]);
								remplacer_var(racine->fd->fd,(int)racine->fg->val,tab_cte[indice_mem]);
								assertion_af(racine->fd->fg->fd->fg,NULL,verite);
								assertion_af(racine->fd->fd,NULL,verite);
								return 1;
								}
							else
								return 0;
							}}
					}}}
			}}}
	}}}
	return -1;
}





/* Assertion (dans le modele) d'une formule.
 * Argument:
 * 	- racine: formule traitee.
 *	- verite: 0 ou 1 (resp. negation ou affirmation).
 * Algorithme:
 * 	- SWITCH du type de racine:
 *		AF: appliquer assertion_af() avec comme argument "racine" et une "liste vide d'entiers".
 *		LAMBDA: non traite, car on suppose que la beta-reduction nous a debarasse des noeuds de type LAMBDA.
 *		QUANT: appliquer la fonction correspondante à la valeur 0 ou 1 (resp. existentiel ou universel) sur "racine".
 *		OP1: appliquer assertiopn() sur le fils gauche de "racine" et la valeur inverse de "verite".
 *		OP2: 
 *			SWITCH de la valeur de OP2:
 *				- "et": appliquer assertion() sur le fils gauche de "racine" et "verite".
 *				- "implies": appliquer assertion_imp() sur "racine" et "verite".
 *				- "ou": ne rien faire.
 */
void assertion(noeud * racine, int verite){
	//printf("\nASSERTION\n");
    if (racine == NULL){
        printf("racine == NULL");
        return ;}
    switch (racine->type) {
        case AF:
	       assertion_af(racine,NULL,verite);
            break ;
        case LAMBDA:
            printf("MOD : case LAMBDA non traite -> Beta reduction.\n");
            break ;
        case QUANT :
            switch(racine->val){
                case 1: //some
      		        
      		        switch(presupposition(racine,verite)){
      		        	case -1:
      		        		printf("MOD : case IL_EXISTE non traite -> Combinatoire des mondes possibles.\n");
      		        		break;
      		        	case 0:
      		        		printf("MOD : Presupposition: fausse.\n");
      		        		break;
      		        	case 1: printf("MOD : Presupposition: vraie.\n");
      		        		break;
      		        	}
                    break;
                case 2: //all
                	assertion_univers(racine,verite);
                    break;
                }
            break ;
        case OP1 : 
        	assertion(racine->fg,val_not(verite));        	
            	break ;
        case OP2 :
        	switch(racine->val){
                case 1: // et
        			assertion(racine->fg,verite);
 			       	assertion(racine->fd,verite);
        			break;
        		case 2: // ou
        		    printf("MOD : case OU non traite -> Combinatoire des mondes possibles.\n");
         			break;
		          case 3: // implies
        			assertion_imp(racine,verite);
        			break;
        	}
            break ;
    }
}

/* Assertion (dans le modele) d'une formule ne contenant que des variables "constantifiees".
 * Argument:
 * 	- racine: formule traitee.
 *	- verite: 0 ou 1 (resp. negation ou affirmation).
 * Algorithme:
 * 	- SWITCH du type de racine:
 *		AF: appliquer assertion_af() avec comme argument "racine" et une "liste vide d'entiers".
 *		LAMBDA: non traite, car on suppose que la beta-reduction nous a debarasse des noeuds de type LAMBDA.
 *		QUANT: appliquer la fonction correspondante à la valeur 0 ou 1 (resp. existentiel ou universel) sur "racine".
 *		OP1: appliquer assertion_sans_var() sur le fils gauche de "racine" et la valeur inverse de "verite".
 *		OP2: 
 *			SWITCH de la valeur de OP2:
 *				- "et": appliquer assertion_sans_var() sur le fils gauche de "racine" et "verite".
 *				- "implies": appliquer assertion_imp_sans_var() sur "racine" et "verite".
 *				- "ou": ne rien faire.
 */
int assertion_sans_var(noeud * racine, int verite){
	//printf("\n***ASSERTION SS VAR***\n");
	//affiche_formule(racine);
    if (racine == NULL){
        printf("MOD : racine == NULL");
        return ;}
        //printf("TYPE: %i\n",racine->type);
        //getchar();
    switch (racine->type) {
        case AF:
	       assertion_af(racine,NULL,verite);
            break ;
        case LAMBDA:
            printf("MOD : case LAMBDA non traite -> Beta reduction.\n");
            break ;
        case QUANT :
            assertion_sans_var(racine->fd,verite);
            break ;
        case OP1 : 
               	assertion_sans_var(racine->fg,val_not(verite));
	        break ;
        case OP2 :
        	switch(racine->val){
                case 1: // et
        			assertion_sans_var(racine->fg,verite);
        			assertion_sans_var(racine->fd,verite);
        			break;
        	case 2: // ou
				printf("MOD : case OU non traite -> Combinatoire des mondes possibles.\n");
         			break;
		case 3: // implies
        			assertion_imp_sans_var(racine,verite);
        			break;
        	}
            break ;
    }
}

/* Assertion d'une formule au modele.
 * Argument:
 * - racine: formule traitee.
 */
void faire_assertion(noeud* racine){
	assertion(racine,1);
}
